$\forall$$A$:Type, $d$:EqDecider($A$), $i$:$A$. sqequal((eqof($d$)($i$,$i$)); tt)